package src;


import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;


//This class contains the code for unifying two expressions

public class UNIFY {
	
	//A variable that is set to true for regular mode, in which only the final answer is given
	// and is set to true for trace mode to get each sub-answer
	static boolean trace = false ;
	
	
	//A method that takes two expressions and returns their most common unifier
	public static ArrayList<String> unify(String exp_1, String exp_2)
			throws Exception {
		
		exp_1 = exp_1.toLowerCase();
		exp_2 = exp_2.toLowerCase();
		
		
		//If from the start the two expressions are not of the same function it terminates
		if (exp_1.charAt(0) != exp_2.charAt(0))
			throw new Exception("Two expressions cannot be unified");

		
		//removing the first and last brackets
		exp_1 = exp_1.substring(2, exp_1.length() - 1);
		exp_2 = exp_2.substring(2, exp_2.length() - 1);

		//splitting the expressions to get each instance seperatly
		List<String> list_1 = new ArrayList<String>(Arrays.asList(exp_1
				.split(";")));
		List<String> list_2 = new ArrayList<String>(Arrays.asList(exp_2
				.split(";")));

		
		//If the number of instances of the two expressions are different 
		//then the the functions fails
		if (list_1.size() != list_2.size())
		{
			if(trace)
				System.out.println("Cannot unify expressions of different sizes");
			throw new Exception("Two expresions cannot be unified");
		}
		
		
		ArrayList<String> mgu = new ArrayList<String>();
		
		ArrayList<ArrayList<String>> ll_1 = new ArrayList<ArrayList<String>>();
		ArrayList<ArrayList<String>> ll_2 = new ArrayList<ArrayList<String>>();
		
		
		//transforming each instance into a list to have a list of lists
		for(String e : list_1)
		{
			ll_1.add(listify(e));
		}
		
		for(String e : list_2)
		{
			ll_2.add(listify(e));
		}
		

		return unify_helper(ll_1, ll_2, mgu);
	}

	
	
	//the recursive method that returns the most general unifier for each step 
	public static ArrayList<String> unify_helper(ArrayList<ArrayList<String>> list_1,
			ArrayList<ArrayList<String>> list_2, ArrayList<String> mgu) throws Exception {

		//If the lists are empty them the recursive call is done
		if (list_1.isEmpty()||list_2.isEmpty())
			return mgu;

		
		//In case we are matching just exactly two instances that in the previous
		//steps neither of them was a variable
		//and not both of them are constants, and then we reached a point 
		// were one of them is an atom after removing the common function symbols,
		//we flatten the other to one inner list continue unifying
		
		if(list_1.size()==1 && list_2.size()>1)
		{
			ArrayList<ArrayList<String>> temp = list_2;
			ArrayList<String> t = new ArrayList<String>();
			list_2.removeAll(temp);
			for(ArrayList<String> e : temp)
			{
				t.addAll(e);
			}
			list_2.add(t);
		}
		
		if(list_2.size()==1 && list_1.size()>1)
		{
			ArrayList<ArrayList<String>> temp = list_1;
			ArrayList<String> t = new ArrayList<String>();
			list_1.removeAll(temp);
			for(ArrayList<String> e : temp)
			{
				t.addAll(e);
			}
			list_2.add(t);
		}
	//	System.out.println(list_1 + " : " + list_2);

		ArrayList<String> exp_1 = list_1.remove(0);
		ArrayList<String> exp_2 = list_2.remove(0);


		//If both instances are equal, then we continue with the rest of the list
		if (exp_1.equals(exp_2))
			return unify_helper(list_1, list_2, mgu);

		//If both are instances and not equal ^^ , then fail
		if (exp_1.size() == 1 && exp_1.get(0).compareTo("m") < 0
				&& exp_2.size() == 1 && exp_2.get(0).compareTo("m") < 0)
		{
			if(trace)
				System.out.println("Trying to unify two atoms");
			throw new Exception("Two expresions cannot be unified");
		}

		
		//If either of them is a variable, we find a substitution else we 
		//listify the two expressions, find their mgu and use the result as the
		//input for another recursive call
		if (exp_1.size() == 1 && exp_1.get(0).compareTo("m") >= 0)
			uniVar(exp_1.get(0), string(exp_2), mgu);
		else if (exp_2.size() == 1 && exp_2.get(0).compareTo("m") >= 0)
			uniVar(exp_2.get(0), string(exp_1), mgu);
		else
		{
			if (exp_1.size()>1&&exp_2.size()>1)
				if(exp_1.get(0)!=exp_2.get(0))
				{	if(trace)
						System.out.println("Cannot unify two different functions");
					throw new Exception("Two expresions cannot be unified");
				}
					
			return unify_helper(list_1, list_2,
					unify_helper(listifyList(exp_1), listifyList(exp_2), mgu));
		}

		
		//recursive call for the rest of the lists
		return unify_helper(list_1, list_2, mgu);
	}

	
	// A method that takes a list of strings and transforms it to a string
	public static String string(ArrayList<String> exp_2) {

		
		String result = "";
		for(String e : exp_2)
			result=result+e;

		return result;
	}

	
	// a function that takes two expressions and adds their substitution 
	//if exists to the most general unifier
	public static void uniVar(String exp_1, String exp_2, ArrayList<String> mgu)
			throws Exception {

		String new_uni = exp_2 + "/" + exp_1;

		//If the sub. is already their continue
		if (mgu.contains(new_uni))
			return;

		//If their exists a sub. in mgu for exp_1 already,
		//unify it with exp_2
		for (String e : mgu) {
			if (e.endsWith(exp_1)) {
				ArrayList<String> l_1 = listify(e.substring(0, e.length() - 2));
				ArrayList<String> l_2 = listify(exp_2);
				unify_helper(listifyList(l_1), listifyList(l_2), mgu);
				return;
			}
		}

		String t = exp_2;

		// make substitutions in exp_2 according to the mcu
		for (String e : mgu) {
			t = t.replace(e.charAt(e.length() - 1) + "",
					e.substring(0, e.length() - 2));
		}

		//If after sub, exp_1 appears in exp_2, then we cannot unify,
		//as we're trying to unify exp_1 with an instance of its self
		if (t.contains(exp_1))
		{
			if(trace)
				System.out.println("Expression tries to unify with an instance of itself");
			throw new Exception("Two expresions cannot be unified");
		}
		else
		{
			if(trace)
			System.out.println("Most General Unifier so far : " + mgu);
			
			//add the new sub. to the mgu
			mgu.add(t + "/" + exp_1);
			
			if(trace)
				System.out.println("Therefor Unifing " + exp_1 + " and " + exp_2 + " gives : " + t + "/" + exp_1);
		
		}

	}

	
	//this method takes a string and return a list of each character alone
	public static ArrayList<String> listify(String x) {
		ArrayList<String> result = new ArrayList<String>();

		for (int i = 0; i < x.length(); i++) {
			char e = x.charAt(i);

			if (Character.isLetter(e))
				result.add(e + "");
		}

		return result;
	}

	//takes a list of strings, it takes each string in it put it in a list, and returns a list of them
	public static ArrayList<ArrayList<String>> listifyList(ArrayList<String> x)
	{
		ArrayList<ArrayList<String>> result = new ArrayList<ArrayList<String>>();
		
		for(String e : x)
		{
			ArrayList<String> temp = new ArrayList<String>();
			temp.add(e);
			result.add(temp);
			
		}
		
		return result;
	}
	
	
	public static void main(String[] args)
	{
		
		String exp_1 = "";
		String exp_2 = "";
		try {
			  exp_1 =  "P(x; g(x); g(f(a))";
			  exp_2 = "P(f(u); v; v)";
			 System.out.println("Most general unifier for ( "+ exp_1 +" and " + exp_2+ " ) is :" + "\n" 
					 + unify(exp_1, exp_2));
			 
			  exp_1 =  "P(a; y; f(y))";
			  exp_2 = "P(z; z; u)";
			  System.out.println("Most general unifier for ( "+ exp_1 +" and " + exp_2+ " ) is :" + "\n" 
						 + unify(exp_1, exp_2));
			  
			  exp_1 =  "f(x; g(x); x)";
			  exp_2 = "f(g(u); g(g(z)); z)";
			  System.out.println("Most general unifier for ( "+ exp_1 +" and " + exp_2+ " ) is :" + "\n" 
						 + unify(exp_1, exp_2));
			  
			 } catch (Exception e) {
			 // TODO Auto-generated catch block
			 System.out.println( exp_1 + " and " + exp_2 + " cannot be unified");
			 }	
	}
}
